declare
class Victim 
   attr ident step last succ pred alive:true 
   meth init(I K L) ident:=I step:=K last:=L end 
   meth setSucc(S) succ:=S end 
   meth setPred(P) pred:=P end 
   meth kill(X S) 
      if @alive then 
         if S==1 then @last=@ident 
         elseif X mod @step==0 then 
            alive:=false 
            {@pred setSucc(@succ)} 
            {@succ setPred(@pred)} 
            {@succ kill(X+1 S-1)} 
         else 
            {@succ kill(X+1 S)} 
         end 
      else {@succ kill(X S)} end 
   end
end

fun {Josephus N K}
   A={NewArray 1 N null}
   Last
in
   for I in 1..N do
      A.I:={NewActive Victim init(I K Last)}
   end
   for I in 2..N do {A.I setPred(A.(I-1))} end
   {A.1 setPred(A.N)}
   for I in 1..(N-1) do {A.I setSucc(A.(I+1))} end
   {A.N setSucc(A.1)} {A.1 kill(1 N)}
   Last
end
